\begin{tabbing}
$y$=$f$$\ast$($x$) via $L$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(0 $<$ $\parallel$$L$$\parallel$)\+
\\[0ex]\& $y$ = hd($L$)
\\[0ex]\& $x$ = last($L$)
\\[0ex]\& ($\forall$$i$:\{0..($\parallel$$L$$\parallel$ {-} 1)$^{-}$\}. $L$[$i$] = $f$($L$[($i$+1)]) \& ($\neg$($L$[$i$] = $L$[($i$+1)])))
\-
\end{tabbing}